/* 
 * $Id: AdjustmentNode.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright 2004
 *    Distributed Systems Research Group
 *    Department of Software Engineering
 *    Faculty of Mathematics and Physics
 *    Charles University, Prague
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 */

package org.objectweb.fractal.bpc.checker.node;

import java.util.TreeSet;
import java.util.ArrayList;
import java.util.TreeMap;
import java.util.Iterator;

import org.objectweb.fractal.bpc.checker.DFSR.CheckingException;
import org.objectweb.fractal.bpc.checker.state.*;
import org.objectweb.fractal.bpc.checker.utils.AnotatedProtocol;


/**
 * Adjustment node represent the adjustment operator
 */
public class AdjustmentNode extends TreeNode {

    /** Creates a new instance of AdjustmentNode */
    public AdjustmentNode(TreeNode node1, TreeNode node2, TreeSet events) {
        //super(getUnion(node1, node2));
        super("(" + node1.protocol + ") " + "|S|" + " (" + node2.protocol + ")");
        this.events = events;
        this.nodes = new TreeNode[2];
        this.nodes[0] = node1;
        this.nodes[1] = node2;
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getInitial()
     */
    public State getInitial() {
        State[] states = new State[2];
        states[0] = nodes[0].getInitial();
        states[1] = nodes[1].getInitial();

        return new CompositeState(states);
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#isAccepting(org.objectweb.fractal.bpc.checker.state.State)
     */
    public boolean isAccepting(State state) {
        CompositeState cstate = (CompositeState) state;

        return (nodes[0].isAccepting(cstate.states[0])) && (nodes[1].isAccepting(cstate.states[1]));
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getTransitions(org.objectweb.fractal.bpc.checker.state.State)
     */
    public TransitionPairs getTransitions(State state) throws InvalidParameterException, CheckingException {
        CompositeState cstate = (CompositeState) state;

        TransitionPair[] trans1 = nodes[0].getTransitions(cstate.states[0]).transitions;
        TransitionPair[] trans2 = nodes[1].getTransitions(cstate.states[1]).transitions;

        ArrayList result = new ArrayList();
        TreeMap sync = new TreeMap();

        //we divide the transitions of node1 (states[0]) into two groups
        // - that of not present within the events set and the others
        for (int i = 0; i < trans1.length; ++i) {
            Integer key = new Integer(trans1[i].eventIndex);
            Integer basekey = new Integer(ActionRepository.getPure(key.intValue()));

            if (events.contains(basekey))
                if (sync.containsKey(key))
                    ((ArrayList) sync.get(key)).add(trans1[i]);
                else {
                    ArrayList value = new ArrayList();
                    value.add(trans1[i]);
                    sync.put(new Integer(trans1[i].eventIndex), value);
                }
            else {
                State[] states = new State[2];
                states[0] = trans1[i].state;
                states[1] = cstate.states[1];

                result.add(new TransitionPair(trans1[i].eventIndex, new CompositeState(states)));
            }
        }

        // now complete the result array
        for (int i = 0; i < trans2.length; ++i) {
            Integer key = new Integer(trans2[i].eventIndex);
            Integer basekey = new Integer(ActionRepository.getPure(key.intValue()));

            if (events.contains(basekey)) {
                if (sync.containsKey(key)) {
                    Iterator it = ((ArrayList) sync.get(key)).iterator();

                    while (it.hasNext()) {
                        State[] states = new State[2];
                        states[0] = ((TransitionPair) it.next()).state;
                        states[1] = trans2[i].state;

                        result.add(new TransitionPair(trans2[i].eventIndex, new CompositeState(states)));
                    }
                }
            }

            else {
                State[] states = new State[2];
                states[0] = cstate.states[0];
                states[1] = trans2[i].state;

                result.add(new TransitionPair(trans2[i].eventIndex, new CompositeState(states)));
            }
        }

        TransitionPair[] result1 = new TransitionPair[result.size()];
        Iterator it = result.iterator();
        int i = 0;

        while (it.hasNext())
            result1[i++] = (TransitionPair) it.next();

        return new TransitionPairs(result1);
    }

    /**
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getWeight()
     */
    public long getWeight() {
        if (weight != -1)
            return weight;
        else {
            return weight = nodes[0].getWeight() * nodes[1].getWeight();
        }
    }

    /**
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#forwardCut(java.util.TreeSet)
     */
    public TreeNode forwardCut(TreeSet livingevents) {
        TreeSet exlivev = new TreeSet(livingevents);

        exlivev.addAll(events);
        TreeSet exlivev2 = new TreeSet(exlivev);

        nodes[0] = nodes[0].forwardCut(exlivev);
        nodes[1] = nodes[1].forwardCut(exlivev2);

        if ((nodes[0] == null) || (nodes[1] == null))
            return null;

        else
            return this;
    }

    /**
     * @return the symbolic name of the treenode denoting its type
     */
    public String[] getTypeName() {
        String[] result = { "Adjustment", "/" };
        return result;
    }

    /**
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getAnotatedProtocol(org.objectweb.fractal.bpc.checker.state.State)
     */
    public AnotatedProtocol getAnotatedProtocol(State state) {
        throw new RuntimeException(this.getClass().getName() + ".getAnotatedProtocol is not implemented");
    }

    //--------------------------------------------------------------------------

    /**
     * The set of event for composition operator
     */
    final private TreeSet events;


}
